| Nuprl Lemma : int_2 |
13,42 |
|
COM: int_2_begin
COM: int_2_summary
COM: int_2_intro
STM: int trichot
STM: le transitivity
STM: lt transitivity 1
STM: lt transitivity 2
STM: eq to le
STM: lt to le
STM: le to lt weaken
STM: lt to le rw
STM: le to lt
STM: le to lt rw
STM: add ident
STM: add com
STM: add functionality wrt le
STM: add functionality wrt lt
STM: add functionality wrt eq
STM: add cancel in eq
STM: add cancel in lt
STM: add cancel in le
STM: add mono wrt eq
STM: add mono wrt eq rw
STM: add mono wrt lt
STM: add mono wrt lt rw
STM: add mono wrt le
STM: add mono wrt le rw
STM: minus functionality wrt le
STM: minus mono wrt le
STM: minus functionality wrt eq
STM: minus mono wrt eq
STM: minus functionality wrt lt
STM: minus mono wrt lt
STM: sub functionality wrt le
STM: minus minus cancel
STM: mul ident
STM: mul com
STM: zero ann
STM: zero ann a
STM: zero ann b
STM: minus thru mul
STM: mul preserves eq
STM: mul preserves lt
STM: mul preserves le
STM: mul cancel in eq
STM: mul cancel in lt
STM: mul cancel in le
COM: mul_fun_comment
STM: multiply functionality wrt le
STM: mul functionality wrt eq
STM: int entire
STM: int entire a
STM: mul bounds 1a
STM: mul bounds 1b
STM: pos mul arg bounds
STM: neg mul arg bounds
COM: add_nat_wf_com
STM: add nat wf
STM: multiply nat wf
COM: quasi_lin_com
ABS: |i|
STM: absval wf
STM: comb for absval wf
STM: absval pos
STM: absval neg
ABS: i = 
j
STM: pm equal wf
STM: absval zero
STM: absval ubound
STM: absval lbound
STM: absval eq
STM: absval sym
STM: absval elim
ABS: imax(a;b)
STM: imax wf
STM: comb for imax wf
ABS: imin(a;b)
STM: imin wf
STM: comb for imin wf
STM: minus imax
STM: minus imin
STM: imax lb
STM: imax ub
STM: imax add r
STM: imax assoc
STM: imax com
STM: imin assoc
STM: imin com
STM: imin add r
STM: imin lb
STM: imin ub
ABS: a -- b
STM: ndiff wf
STM: comb for ndiff wf
STM: ndiff id r
STM: ndiff ann l
STM: ndiff inv
STM: ndiff ndiff
STM: ndiff ndiff eq imin
STM: ndiff add eq imax
STM: ndiff zero
COM: div_rem_com
STM: div rem sum
STM: rem to div
COM: quadrants_com
STM: rem bounds 1
STM: rem bounds 2
STM: rem bounds 3
STM: rem bounds 4
STM: div 2 to 1
STM: div 3 to 1
STM: div 4 to 1
STM: rem 2 to 1
STM: rem 3 to 1
STM: rem 4 to 1
STM: rem sym
STM: rem antisym
STM: remainder wf
STM: comb for remainder wf
STM: rem bounds z
STM: rem sym 1
STM: rem sym 1a
STM: rem sym 2
STM: rem mag bound
STM: div bounds 1
STM: divide wf
STM: divide wfa
ABS: Div(a;n;q)
STM: div nrel wf
STM: div fun sat div nrel
STM: div elim
STM: div unique
STM: div lbound 1
ABS: Rem(a;n;r)
STM: rem nrel wf
STM: rem fun sat rem nrel
STM: div base case
STM: div rec case
STM: rem base case
STM: rem gen base case
STM: rem rec case
STM: rem invariant
STM: rem addition
STM: rem rem to rem
STM: rem base case z
STM: rem eq args
STM: rem eq args z
ABS: a mod n
STM: modulus wf
ABS: a 
n
STM: div floor wf
STM: mod bounds
STM: div floor mod sum
STM: int mag well founded
STM: int upper well founded
STM: int upper ind
STM: int lower well founded
STM: int lower ind
STM: int seg well founded up
STM: int seg ind
STM: int seg well founded down
STM: decidable ex int seg
STM: decidable all int seg
COM: int_2_end
